Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    function(iszero,0,dummy,dummy2)  → true
2:    function(iszero,s(x),dummy,dummy2)  → false
3:    function(p,0,dummy,dummy2)  → 0
4:    function(p,s(0),dummy,dummy2)  → 0
5:    function(p,s(s(x)),dummy,dummy2)  → s(function(p,s(x),x,x))
6:    function(plus,dummy,x,y)  → function(if,function(iszero,x,x,x),x,y)
7:    function(if,true,x,y)  → y
8:    function(if,false,x,y)  → function(plus,function(third,x,y,y),function(p,x,x,y),s(y))
9:    function(third,x,y,z)  → z
There are 6 dependency pairs:
10:    FUNCTION(p,s(s(x)),dummy,dummy2)  → FUNCTION(p,s(x),x,x)
11:    FUNCTION(plus,dummy,x,y)  → FUNCTION(if,function(iszero,x,x,x),x,y)
12:    FUNCTION(plus,dummy,x,y)  → FUNCTION(iszero,x,x,x)
13:    FUNCTION(if,false,x,y)  → FUNCTION(plus,function(third,x,y,y),function(p,x,x,y),s(y))
14:    FUNCTION(if,false,x,y)  → FUNCTION(third,x,y,y)
15:    FUNCTION(if,false,x,y)  → FUNCTION(p,x,x,y)
The approximated dependency graph contains 2 SCCs: {10} and {11,13}.
Tyrolean Termination Tool  (1.11 seconds)   ---  May 3, 2006